<!DOCTYPE html>
<html class="writer-html5" lang="en" >
<head>
  <meta charset="utf-8" /><meta name="generator" content="Docutils 0.17.1: http://docutils.sourceforge.net/" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>Index of Lean tactics &mdash; The Mechanics of Proof, by Heather Macbeth</title>
      <link rel="stylesheet" href="_static/pygments.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/theme.css" type="text/css" />
      <link rel="stylesheet" href="_static/css/custom.css" type="text/css" />
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script data-url_root="./" id="documentation_options" src="_static/documentation_options.js"></script>
        <script src="_static/jquery.js"></script>
        <script src="_static/underscore.js"></script>
        <script src="_static/doctools.js"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="Transitioning to mainstream Lean" href="Mainstream_Lean.html" />
    <link rel="prev" title="10. Relations" href="10_Relations.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >
            <a href="index.html" class="icon icon-home"> The Mechanics of Proof
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul>
<li class="toctree-l1"><a class="reference internal" href="00_Introduction.html">Preface</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="01_Proofs_by_Calculation.html">1. Proofs by calculation</a></li>
<li class="toctree-l1"><a class="reference internal" href="02_Proofs_with_Structure.html">2. Proofs with structure</a></li>
<li class="toctree-l1"><a class="reference internal" href="03_Parity_and_Divisibility.html">3. Parity and divisibility</a></li>
<li class="toctree-l1"><a class="reference internal" href="04_Proofs_with_Structure_II.html">4. Proofs with structure, II</a></li>
<li class="toctree-l1"><a class="reference internal" href="05_Logic.html">5. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="06_Induction.html">6. Induction</a></li>
<li class="toctree-l1"><a class="reference internal" href="07_Number_Theory.html">7. Number theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="08_Functions.html">8. Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="09_Sets.html">9. Sets</a></li>
<li class="toctree-l1"><a class="reference internal" href="10_Relations.html">10. Relations</a></li>
</ul>
<ul class="current">
<li class="toctree-l1 current"><a class="current reference internal" href="#">Index of Lean tactics</a></li>
<li class="toctree-l1"><a class="reference internal" href="Mainstream_Lean.html">Transitioning to mainstream Lean</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">The Mechanics of Proof</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home"></a> &raquo;</li>
      <li>Index of Lean tactics</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/Index_of_Tactics.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="index-of-lean-tactics">
<span id="tactic-index"></span><h1>Index of Lean tactics<a class="headerlink" href="#index-of-lean-tactics" title="Permalink to this headline">&#61633;</a></h1>
<p>Tactics marked * are specific to this book, so you will not be able to get help with them by
googling/consulting internet forums/etc.  Reread the indicated part of the book or ask
your instructor!</p>
<p class="rubric">* <code class="docutils literal notranslate"><span class="pre">addarith</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#shortcut"><span class="std std-numref">Section 1.5</span></a>)</p>
<p>Attempts to solve an equality or inequality by moving terms from the left-hand side to the
right-hand side, or vice versa.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">apply</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#lemmas"><span class="std std-numref">Section 2.2</span></a>; for <span class="math notranslate nohighlight">\(\forall\)</span> and <span class="math notranslate nohighlight">\(\to\)</span> hypotheses, <a class="reference internal" href="04_Proofs_with_Structure_II.html#forall-implies"><span class="std std-numref">Section 4.1</span></a>)</p>
<p>Invokes a specified lemma or hypothesis to modify the goal.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">by_cases</span></code> (first use: <a class="reference internal" href="05_Logic.html#lem"><span class="std std-numref">Section 5.2</span></a>)</p>
<p>Case-splits on whether a given statement is true or false.</p>
<p class="rubric">* <code class="docutils literal notranslate"><span class="pre">cancel</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#tactic-mode"><span class="std std-numref">Section 2.1</span></a>)</p>
<p>Cancels a common factor from LHS/RHS of equality/inequality, cancels an exponentiation common to both sides, etc.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">constructor</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#and"><span class="std std-numref">Section 2.4</span></a>; for <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> goals: <a class="reference internal" href="04_Proofs_with_Structure_II.html#iff"><span class="std std-numref">Section 4.2</span></a>)</p>
<p>Splits an &#8220;and&#8221; goal (<span class="math notranslate nohighlight">\(\land\)</span>) into sub-goals for its left and right parts.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">contradiction</span></code> (first use: <a class="reference internal" href="04_Proofs_with_Structure_II.html#contradiction-hyp"><span class="std std-numref">Section 4.4</span></a>)</p>
<p>If there are two contradictory hypotheses available, this concludes the proof.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">dsimp</span></code> (first use: <a class="reference internal" href="03_Parity_and_Divisibility.html#parity"><span class="std std-numref">Section 3.1</span></a>)</p>
<p>Unfolds a definition.  Typically used while working on a proof rather than in the final version; it
is useful for inspecting a goal or hypothesis more carefully, but in most cases the proof will still
work after a <code class="docutils literal notranslate"><span class="pre">dsimp</span></code> line is deleted.</p>
<p class="rubric">* <code class="docutils literal notranslate"><span class="pre">extra</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#proving-inequalities"><span class="std std-numref">Section 1.4</span></a>; for congruences: <a class="reference internal" href="03_Parity_and_Divisibility.html#using-modular"><span class="std std-numref">Section 3.4</span></a>)</p>
<p>A comparison tactic for inequalities, or other relations such as congruences: checks an inequality
whose two sides differ by the addition of a positive quantity, a congruence mod 3 whose two sides
differ by a multiple of 3, etc.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">interval_cases</span></code> (first use: <a class="reference internal" href="04_Proofs_with_Structure_II.html#forall-implies"><span class="std std-numref">Section 4.1</span></a>)</p>
<p>Given a natural-number or integer variable <span class="math notranslate nohighlight">\(n\)</span> for which numeric upper and lower bounds are
available, produce cases for each of the numeric possibilities for <span class="math notranslate nohighlight">\(n\)</span>.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">intro</span></code> (first use: <a class="reference internal" href="04_Proofs_with_Structure_II.html#forall-implies"><span class="std std-numref">Section 4.1</span></a>; for <span class="math notranslate nohighlight">\(\lnot\)</span> goals: <a class="reference internal" href="04_Proofs_with_Structure_II.html#contradiction"><span class="std std-numref">Section 4.5</span></a>)</p>
<p>Introduces a universally quantified variable (<span class="math notranslate nohighlight">\(\forall\)</span>) or the antecedent of an implication
(<span class="math notranslate nohighlight">\(\to\)</span>) from the goal, or assumes (for the sake of contradiction) the positive version of a
negation (<span class="math notranslate nohighlight">\(\lnot\)</span>) goal.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">left</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#or"><span class="std std-numref">Section 2.3</span></a>)</p>
<p>Selects the left alternative of an &#8220;or&#8221; goal (<span class="math notranslate nohighlight">\(\lor\)</span>).</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">have</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#tactic-mode"><span class="std std-numref">Section 2.1</span></a>; with a lemma: <a class="reference internal" href="02_Proofs_with_Structure.html#or"><span class="std std-numref">Section 2.3</span></a>; introducing a new goal: <a class="reference internal" href="02_Proofs_with_Structure.html#and"><span class="std std-numref">Section 2.4</span></a>)</p>
<p>Records a fact (followed by the proof of that fact), which then becomes available as an
extra hypothesis.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">mod_cases</span></code> (first use: <a class="reference internal" href="03_Parity_and_Divisibility.html#using-modular"><span class="std std-numref">Section 3.4</span></a>)</p>
<p>Introduces cases for a variable according to its residue modulo a specified number.</p>
<p class="rubric">* <code class="docutils literal notranslate"><span class="pre">numbers</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#proving-inequalities"><span class="std std-numref">Section 1.4</span></a>; with <code class="docutils literal notranslate"><span class="pre">at</span></code> for contradictions: <a class="reference internal" href="04_Proofs_with_Structure_II.html#contradiction-hyp"><span class="std std-numref">Section 4.4</span></a>)</p>
<p>Proves numeric facts, like <span class="math notranslate nohighlight">\(3\cdot 12 &lt; 13 + 25\)</span> or <span class="math notranslate nohighlight">\(3\cdot 5+1=4\cdot 4\)</span>.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">obtain</span></code> (first use for <span class="math notranslate nohighlight">\(\lor\)</span>: <a class="reference internal" href="02_Proofs_with_Structure.html#or"><span class="std std-numref">Section 2.3</span></a>; for <span class="math notranslate nohighlight">\(\land\)</span>: <a class="reference internal" href="02_Proofs_with_Structure.html#and"><span class="std std-numref">Section 2.4</span></a>; for <span class="math notranslate nohighlight">\(\exists\)</span>: <a class="reference internal" href="02_Proofs_with_Structure.html#exists"><span class="std std-numref">Section 2.5</span></a>)</p>
<p>Takes apart a hypothesis of the form &#8220;or&#8221; (<span class="math notranslate nohighlight">\(\lor\)</span>), &#8220;and&#8221; (<span class="math notranslate nohighlight">\(\land\)</span>) or &#8220;there exists&#8221;
(<span class="math notranslate nohighlight">\(\exists\)</span>).</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">push_neg</span></code> (first use: <a class="reference internal" href="05_Logic.html#negation-normalize"><span class="std std-numref">Section 5.3</span></a>)</p>
<p>Converts a hypothesis or goal to a logically equivalent form with negations pushed inwards as far
as possible.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">rel</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#proving-inequalities"><span class="std std-numref">Section 1.4</span></a>; for congruences: <a class="reference internal" href="03_Parity_and_Divisibility.html#using-modular"><span class="std std-numref">Section 3.4</span></a>; for logical equivalences: <a class="reference internal" href="05_Logic.html#negation-normalize"><span class="std std-numref">Section 5.3</span></a>)</p>
<p>A &#8220;substitution-like&#8221; tactic for inequalities, or other relations such as congruences: looks for
the left-hand side of a specified inequality (or congruence, &#8230;) fact in the goal, and replaces it
with the right-hand side of that fact, if that replacement is &#8220;obviously&#8221; a valid inequality
(or modular arithmetic, &#8230;) deduction.  Compare with <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">right</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#or"><span class="std std-numref">Section 2.3</span></a>)</p>
<p>Selects the right alternative of an &#8220;or&#8221; goal (<span class="math notranslate nohighlight">\(\lor\)</span>).</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">ring</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#proving-equalities-in-lean"><span class="std std-numref">Section 1.2</span></a>)</p>
<p>Solves algebraic equality goals such as <span class="math notranslate nohighlight">\((x + y) ^ 2 = x ^ 2 + 2xy + y ^ 2\)</span>, when the proof
is effectively &#8220;expand out both sides and rearrange&#8221;.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">rw</span></code> (first use: <a class="reference internal" href="01_Proofs_by_Calculation.html#proving-equalities-in-lean"><span class="std std-numref">Section 1.2</span></a>; for <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> hypotheses/lemmas: <a class="reference internal" href="04_Proofs_with_Structure_II.html#iff"><span class="std std-numref">Section 4.2</span></a>)</p>
<p>Substitution: looks for the left-hand side of a specified equality fact in the goal, and replaces it with
the right-hand side of that fact.</p>
<p>With <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> hypotheses/lemmas, replaces the left-hand side of the specified <code class="docutils literal notranslate"><span class="pre">&#8596;</span></code> fact with
the right-hand side of that fact.</p>
<p class="rubric"><code class="docutils literal notranslate"><span class="pre">use</span></code> (first use: <a class="reference internal" href="02_Proofs_with_Structure.html#exists"><span class="std std-numref">Section 2.5</span></a>)</p>
<p>Provides a witness to an existential goal (<span class="math notranslate nohighlight">\(\exists\)</span>).</p>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="10_Relations.html" class="btn btn-neutral float-left" title="10. Relations" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="Mainstream_Lean.html" class="btn btn-neutral float-right" title="Transitioning to mainstream Lean" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2022-2024, Heather Macbeth.  All rights reserved.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>